Another indicator is the list of Verplex (Milpitas, CA) customers. The list spans large systems houses and semiconductor suppliers, and includes well-known Electronic Design Automation (EDA) firms. In the first half of 1999, we had seven customers. Today, that number has grown to 150 different electronics companies worldwide.

As anyone doing electronic design today knows, verification becomes increasingly important as the complexity of integrated circuits (ICs) increases. Logic simulation has been used for design verification for many years now, but it's quickly losing its effectiveness. Its performance is too slow and coverage is inadequate. Once a design reaches a quarter-million gates, gate-level simulation starts becoming impractical. At the half-million gate level and above, it becomes too risky to verify designs using traditional methods alone.

Formal verification offers a workable and practical solution. Instead of applying stimuli to a design and comparing its responses with expected results, formal verification examines a design and mathematically proves its functional properties. Unlike simulation, which only reports bugs, formal verification can prove their absence. When errors are found, formal verification can generate counter examples to demonstrate error conditions, allowing designers to complete verification tasks faster.

Equivalence checking (see ISD Magazine's Cover Story, January 2001, p. 28) is a part of the formal verification methodology, detecting functional inconsistencies and providing a reliable way to ensure that the final design implementation does what the register transfer-level (RTL) code specifies it should do. It uses mathematical techniques to determine whether one design representation is functionally equivalent to another and can verify that the final netlist is correct.

Formal verification is flexible and can thus be used throughout the design process. In the design creation phase, it can show that a design satisfies certain properties or can derive functional vectors to demonstrate the violation of such conditions. After a higher-level model is created, a design goes through many implementation steps-logic synthesis, place and route, test logic insertion, and clock tree synthesis. Formal verification can be useful here, too. It's often necessary to tweak the logic to correct timing problems after layout. Formal verification tools can compare two designs and ensure errors weren't introduced during design iteration and revision. Formal verification is useful for comparing designs at different levels of abstraction, such as RTL to gate or transistor netlist.

Formal verification is filling a void in most verification flows by exhaustively assuring that the entire chip design from RTL to GDSII stays functionally consistent, thereby reducing or eliminating the need for lengthy gate-level simulation. Moving forward, advanced formal verification techniques such as model checking will overcome traditional limitations and expand into the mainstream.

The move toward a formal verification methodology in the design environment is real. Design teams are integrating formal verification techniques into their design flows, while application specific integrated circuit vendors are supporting formal verification as part of their standard sign-off procedure.

Michael Chang is president and chief executive officer of Verplex Systems, Inc. He is co-founder and is the key architect of the Verplex product lines. Chang was co-founder and president of Checklogic Systems, Inc., which was acquired by Mentor Graphics in 1993.

Print this story	Send as e-mail